#include <vcc.h>



/*
 * Ghost type STATE for vcc verification. There are four states for tasks in FreeRTOS plus
 * "nonexistent" state to indicate the task does't exist in the system.
 */

_(ghost typedef enum {
    nonexistent = 0,
    ready,
    blocked,
    suspended,
    running
} STATE;)

/*
 * Transition rules specify how to transit the state of tasks.
 */
_(ghost \bool transition[5][5])                                  

_(def \bool Trans()
    {
        //  nonexistent, ready, blocked, suspended, running
        //{{ \false,      \true, \false,  \false,    \true  } // nonexistent
        // { \true,       \false,\false,  \true,     \true  } // ready
        // { \true,       \true, \false,  \true,     \true  } // blocked
        // { \true,       \true, \false,  \false,    \true  } // suspended
        // { \true,       \true, \true,   \true,     \false } // running
        return 
        transition[0][0] == \false && transition[0][1] == \true &&  transition[0][2] == \false && transition[0][3] == \false && transition[0][4] == \true &&  // nonexistent
        transition[1][0] == \true &&  transition[1][1] == \false && transition[1][2] == \false && transition[1][3] == \true &&  transition[1][4] == \true &&  // ready
        transition[2][0] == \true &&  transition[2][1] == \true &&  transition[2][2] == \false && transition[2][3] == \true &&  transition[2][4] == \true &&  // blocked
        transition[3][0] == \true &&  transition[3][1] == \true &&  transition[3][2] == \false && transition[3][3] == \false && transition[3][4] == \true &&  // suspended
        transition[4][0] == \true &&  transition[4][1] == \true &&  transition[4][2] == \true &&  transition[4][3] == \true &&  transition[4][4] == \false;  // running


    }
    )
/*
 * virtul type for given CONTEXT
 */
_(ghost typedef void* CONTEXT;)

/*
 * empty context
 */
_(ghost CONTEXT bare_context;)